\begin{tabbing}
$\forall$$i$, $x$, $y$:Id, $k$:Knd, $T$, $A$, $B$:Type, $f$:($A$$\rightarrow$$B$$\rightarrow$$T$$\rightarrow$$A$).
\\[0ex]$\neg$$y$ $=$ $x$
\\[0ex]$\Rightarrow$ \=@$i$: ma{-}single{-}effect1($x$;$A$;$y$;$B$;$k$;$T$;$f$) $\in$ Dsys\+
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: ma{-}single{-}effect1($x$;$A$;$y$;$B$;$k$;$T$;$f$) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]vartype($i$;$x$) $\subseteq\rho$ $A$ \& vartype($i$;$y$) $\subseteq\rho$ $B$
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ $i$ $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ ($x$ after $e$) $=$ $f$(($x$ when $e$),$y$ when $e$,val($e$)) $\in$ $A$))
\-\-\-\-
\end{tabbing}